T:Type, ll:(T List List).
((concat(ll) = []  (T List)))
 (ll1:T List List
 (l1:T List
 ((concat(ll) = (concat(ll1) @ l1 @ [last(concat(ll))])  (T List)
 (& ll1 @ [(l1 @ [last(concat(ll))])]  ll)) 

latex

Definitions

x:A. B(x), P  Q, t  T, , Top, S  T, x:A. B(x), P & Q, as @ bs, Y, A c B, A, T, True, last(L), SQType(T), {T}, P  Q, P  Q, False, Dec(P), P  Q

Lemmas

concat-nil, not wf, concat-cons, top wf, decidable assert, null wf3, concat wf, assert of null, not functionality wrt iff, assert wf, append nil sq, append wf, last wf, iseg wf, last lemma, cons iseg, nil iseg, null append, band wf, iff transitivity, assert of band, and functionality wrt iff, append assoc sq, squash wf, true wf, length wf1, length append, length zero, non neg length, select append back, select wf, le wf